comment |circumscription of a disjunction|

DECLARE INDVAR x;
DECLARE INDCONST a b;
DECLARE PREDCONST isblock 1;
DECLARE PREDPAR P 1;

AXIOM whichblock:	isblock(a)∨isblock(b);;

*****CIRCUMSCRIBE newaxiom isblock P x IN whichblock;

Circumscription has produced the following new axiom:
newaxiom: ((P(a)∨P(b))∧∀x.(P(x)⊃isblock(x)))⊃∀x.(isblock(x)⊃P(x))

*****∧I newaxiom[P←λx.(x=a)];

1 ((a=a∨b=a)∧∀x.(x=a⊃isblock(x)))⊃∀x.(isblock(x)⊃x=a)  

*****∧I newaxiom[P←λx.(x=b)];

2 ((a=b∨b=b)∧∀x.(x=b⊃isblock(x)))⊃∀x.(isblock(x)⊃x=b)  

*****ASSUME isblock(a);

3 isblock(a)  (3)

*****TAUTEQ x=a⊃isblock(x) 3;

4 x=a⊃isblock(x)  (3)

*****∀I ↑ x;

5 ∀x.(x=a⊃isblock(x))  (3)

*****TAUTEQ ∀x.(isblock(x)⊃x=a) 1,5;

6 ∀x.(isblock(x)⊃x=a)  (3)

*****∀E ↑ x;

7 isblock(x)⊃x=a  (3)

*****TAUTEQ isblock(x)≡x=a 3,7;

8 isblock(x)≡x=a  (3)

*****∀I ↑ x;

9 ∀x.(isblock(x)≡x=a)  (3)

*****ASSUME isblock(b);

10 isblock(b)  (10)

*****TAUTEQ x=b⊃isblock(x) 10;

11 x=b⊃isblock(x)  (10)

*****∀I ↑ x;

12 ∀x.(x=b⊃isblock(x))  (10)

*****TAUTEQ ∀x.(isblock(x)⊃x=b) 2,12;

13 ∀x.(isblock(x)⊃x=b)  (10)

*****∀E ↑ x;

14 isblock(x)⊃x=b  (10)

*****TAUTEQ isblock(x)≡x=b 10,14;

15 isblock(x)≡x=b  (10)

*****∀I ↑ x;

16 ∀x.(isblock(x)≡x=b)  (10)

*****⊃I 3⊃9;

17 isblock(a)⊃∀x.(isblock(x)≡x=a)  

*****⊃I 10⊃↑↑;

18 isblock(b)⊃∀x.(isblock(x)≡x=b)  

*****TAUT ∀x.(isblock(x)≡x=a)∨∀x.(isblock(x)≡x=b) whichblock,17:18;

19 ∀x.(isblock(x)≡x=a)∨∀x.(isblock(x)≡x=b)